$\forall$$A$, $B$:Type, ${\it eq}$:($A$$\rightarrow$$A$$\rightarrow\mathbb{B}$), $f$:($A$$\rightarrow$$B$), $x$:$A$, $v$:$B$. $f$[$x$:=$v$] $\in$ $A$$\rightarrow$$B$